Specification set-union

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   set-basic
with
   

   
   
   functions  { . } : elem → set;
              . ∪ . : set × set → set;
              . ∩ . : set × set → set;
              . \ . : set × set → set;
              . -- . : set × elem → set prio 9 left;
   
   
   
   
   

   

   axioms One :  ⊦ {a}  = ∅ ++ a;
          used for: ls;
          Union :  ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2;
          used for: s, ls, nokodkodax;
          Intersect :  ⊦ a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2;
          used for: s, ls, nokodkodax;
          Difference :  ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2;
          used for: s, ls, nokodkodax;
          Delete :  ⊦ a ∈ s -- b ↔ a ≠ b ∧ a ∈ s;
          used for: s, ls, nokodkodax;

   

   
end enrich